0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 285 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 16 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 1 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
fC_in_gga([], [], []) → fC_out_gga([], [], [])
fC_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gA_in_ggga([], T404, T405, .(T404, T405)) → gA_out_ggga([], T404, T405, .(T404, T405))
gA_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, gA_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, gA_out_ggga(T417, T416, .(T418, T419), T421)) → gA_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fC_out_gga(.(T21, T22), [], T24)
fC_in_gga(.(T472, T473), .(T471, []), T475) → U4_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U4_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fC_out_gga(.(T472, T473), .(T471, []), T475)
fC_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U5_gga(T489, T490, T488, T491, T492, T494, fC_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U5_gga(T489, T490, T488, T491, T492, T494, fC_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fC_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
fC_in_gga([], [], []) → fC_out_gga([], [], [])
fC_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gA_in_ggga([], T404, T405, .(T404, T405)) → gA_out_ggga([], T404, T405, .(T404, T405))
gA_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, gA_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, gA_out_ggga(T417, T416, .(T418, T419), T421)) → gA_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fC_out_gga(.(T21, T22), [], T24)
fC_in_gga(.(T472, T473), .(T471, []), T475) → U4_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U4_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fC_out_gga(.(T472, T473), .(T471, []), T475)
fC_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U5_gga(T489, T490, T488, T491, T492, T494, fC_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U5_gga(T489, T490, T488, T491, T492, T494, fC_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fC_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
FC_IN_GGA(.(T21, T22), [], T24) → U3_GGA(T21, T22, T24, gB_in_gga(T22, T21, T24))
FC_IN_GGA(.(T21, T22), [], T24) → GB_IN_GGA(T22, T21, T24)
GB_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_GGA(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
GB_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → GA_IN_GGGA(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)
GA_IN_GGGA(.(T416, T417), T418, T419, T421) → U1_GGGA(T416, T417, T418, T419, T421, gA_in_ggga(T417, T416, .(T418, T419), T421))
GA_IN_GGGA(.(T416, T417), T418, T419, T421) → GA_IN_GGGA(T417, T416, .(T418, T419), T421)
FC_IN_GGA(.(T472, T473), .(T471, []), T475) → U4_GGA(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
FC_IN_GGA(.(T472, T473), .(T471, []), T475) → GB_IN_GGA(.(T472, T473), T471, T475)
FC_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → U5_GGA(T489, T490, T488, T491, T492, T494, fC_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
FC_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → FC_IN_GGA(.(T491, .(T488, .(T489, T490))), T492, T494)
fC_in_gga([], [], []) → fC_out_gga([], [], [])
fC_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gA_in_ggga([], T404, T405, .(T404, T405)) → gA_out_ggga([], T404, T405, .(T404, T405))
gA_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, gA_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, gA_out_ggga(T417, T416, .(T418, T419), T421)) → gA_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fC_out_gga(.(T21, T22), [], T24)
fC_in_gga(.(T472, T473), .(T471, []), T475) → U4_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U4_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fC_out_gga(.(T472, T473), .(T471, []), T475)
fC_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U5_gga(T489, T490, T488, T491, T492, T494, fC_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U5_gga(T489, T490, T488, T491, T492, T494, fC_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fC_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
FC_IN_GGA(.(T21, T22), [], T24) → U3_GGA(T21, T22, T24, gB_in_gga(T22, T21, T24))
FC_IN_GGA(.(T21, T22), [], T24) → GB_IN_GGA(T22, T21, T24)
GB_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_GGA(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
GB_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → GA_IN_GGGA(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)
GA_IN_GGGA(.(T416, T417), T418, T419, T421) → U1_GGGA(T416, T417, T418, T419, T421, gA_in_ggga(T417, T416, .(T418, T419), T421))
GA_IN_GGGA(.(T416, T417), T418, T419, T421) → GA_IN_GGGA(T417, T416, .(T418, T419), T421)
FC_IN_GGA(.(T472, T473), .(T471, []), T475) → U4_GGA(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
FC_IN_GGA(.(T472, T473), .(T471, []), T475) → GB_IN_GGA(.(T472, T473), T471, T475)
FC_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → U5_GGA(T489, T490, T488, T491, T492, T494, fC_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
FC_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → FC_IN_GGA(.(T491, .(T488, .(T489, T490))), T492, T494)
fC_in_gga([], [], []) → fC_out_gga([], [], [])
fC_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gA_in_ggga([], T404, T405, .(T404, T405)) → gA_out_ggga([], T404, T405, .(T404, T405))
gA_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, gA_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, gA_out_ggga(T417, T416, .(T418, T419), T421)) → gA_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fC_out_gga(.(T21, T22), [], T24)
fC_in_gga(.(T472, T473), .(T471, []), T475) → U4_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U4_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fC_out_gga(.(T472, T473), .(T471, []), T475)
fC_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U5_gga(T489, T490, T488, T491, T492, T494, fC_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U5_gga(T489, T490, T488, T491, T492, T494, fC_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fC_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
GA_IN_GGGA(.(T416, T417), T418, T419, T421) → GA_IN_GGGA(T417, T416, .(T418, T419), T421)
fC_in_gga([], [], []) → fC_out_gga([], [], [])
fC_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gA_in_ggga([], T404, T405, .(T404, T405)) → gA_out_ggga([], T404, T405, .(T404, T405))
gA_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, gA_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, gA_out_ggga(T417, T416, .(T418, T419), T421)) → gA_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fC_out_gga(.(T21, T22), [], T24)
fC_in_gga(.(T472, T473), .(T471, []), T475) → U4_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U4_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fC_out_gga(.(T472, T473), .(T471, []), T475)
fC_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U5_gga(T489, T490, T488, T491, T492, T494, fC_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U5_gga(T489, T490, T488, T491, T492, T494, fC_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fC_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
GA_IN_GGGA(.(T416, T417), T418, T419, T421) → GA_IN_GGGA(T417, T416, .(T418, T419), T421)
GA_IN_GGGA(.(T416, T417), T418, T419) → GA_IN_GGGA(T417, T416, .(T418, T419))
From the DPs we obtained the following set of size-change graphs:
FC_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → FC_IN_GGA(.(T491, .(T488, .(T489, T490))), T492, T494)
fC_in_gga([], [], []) → fC_out_gga([], [], [])
fC_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, gB_in_gga(T22, T21, T24))
gB_in_gga([], T31, .(T31, [])) → gB_out_gga([], T31, .(T31, []))
gB_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → gB_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
gB_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → gB_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
gB_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → gB_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
gB_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → gB_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
gB_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → gB_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
gB_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → gB_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
gB_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
gA_in_ggga([], T404, T405, .(T404, T405)) → gA_out_ggga([], T404, T405, .(T404, T405))
gA_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, gA_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, gA_out_ggga(T417, T416, .(T418, T419), T421)) → gA_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, gA_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → gB_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, gB_out_gga(T22, T21, T24)) → fC_out_gga(.(T21, T22), [], T24)
fC_in_gga(.(T472, T473), .(T471, []), T475) → U4_gga(T472, T473, T471, T475, gB_in_gga(.(T472, T473), T471, T475))
U4_gga(T472, T473, T471, T475, gB_out_gga(.(T472, T473), T471, T475)) → fC_out_gga(.(T472, T473), .(T471, []), T475)
fC_in_gga(.(T489, T490), .(T488, .(T491, T492)), T494) → U5_gga(T489, T490, T488, T491, T492, T494, fC_in_gga(.(T491, .(T488, .(T489, T490))), T492, T494))
U5_gga(T489, T490, T488, T491, T492, T494, fC_out_gga(.(T491, .(T488, .(T489, T490))), T492, T494)) → fC_out_gga(.(T489, T490), .(T488, .(T491, T492)), T494)
FC_IN_GGA(.(T489, T490), .(T488, .(T491, T492)), T494) → FC_IN_GGA(.(T491, .(T488, .(T489, T490))), T492, T494)
FC_IN_GGA(.(T489, T490), .(T488, .(T491, T492))) → FC_IN_GGA(.(T491, .(T488, .(T489, T490))), T492)
From the DPs we obtained the following set of size-change graphs: